nLab metric locale

Definition

A metric locale is a premetric locale such that for all $U:\mathcal{O}(x)$,

$$U =_{\mathcal{O}(x)} \bigvee_{V:\sum_{V':\mathcal{O}(x)} V' \lhd U} V$$

where

$$\sum_{V':\mathcal{O}(x)} V' \lhd U$$

is the subtype of all $V':\mathcal{O}(x)$ such that $V' \lhd U$.

See also

• locale

• premetric locale

• metric space

References

• Simon Henry, Localic Metric spaces and the localic Gelfand duality (arXiv:1411.0898)

• Graham Manuell, Uniform locales and their constructive aspects, (arXiv:2106.00678)